Add Matrix.regularizedInv_mul_tendsto_one and the trace corollaries Matrix.trace_regularizedInv_mul_tendsto and Matrix.trace_regularizedInv_mul_tendsto_card: for a square matrix M over a normed field with det M ≠ 0, the Tikhonov-regularized expression (M + lam • 1)⁻¹ * M tends to the identity matrix as the scalar lam tends to zero, and consequently its trace tends to tr 1 = (Fintype.card d : R). The proofs compose NormedRing.inverse_continuousAt, continuousAt_matrix_inv, Matrix.nonsing_inv_mul, and Continuous.matrix_trace; no new definitions are added. These lemmas are useful in matrix-regularization limit arguments arising in numerical linear algebra (Tikhonov-regularized least squares, ridge regression) and in statistics.

AI-assistance disclosure

Per the Mathlib AI-use policy:

• Tool. Claude Code (Anthropic) with the Claude Sonnet 4.6 model.
• Use. I specified the target lemma statements and the proof strategy; the assistant drafted Lean 4 tactic combinations against current Mathlib. I iterated on the proofs, verified each lemma builds under lake build from a clean checkout, and read the final code.
• Vouching. I have read every declaration in this file and can defend the proofs without further AI assistance. I welcome reviewer feedback on naming, namespace placement, and stylistic alignment with the surrounding Mathlib modules.